ds:x:Id fp Type{i}, da:k:Knd fp Type{i}, P:(ecl(ds;da)Prop{i'}).
(k:Knd, test:(State(ds)Valtype(da;k)). P(eclbase(k;test)))
 (a, b:ecl(ds;da). P(a)  P(b)  P(eclseq(a;b)))
 (a, b:ecl(ds;da). P(a)  P(b)  P(ecland(a;b)))
 (a, b:ecl(ds;da). P(a)  P(b)  P(eclor(a;b)))
 (a:ecl(ds;da). P(a)  P([a]*))
 (a:ecl(ds;da), n:. P(a)  P(a.n))
 (a:ecl(ds;da), n:. P(a)  P(eclthrow(a;n)))
 (a:ecl(ds;da), l: List. P(a)  P(eclcatch(a;l)))
 {x:ecl(ds;da). P(x)} 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), {T}, t  T, x. t(x), ecl(ds;da), eclbase(k;test), eclseq(a;b), ecland(a;b), eclor(a;b), [a]*, a.n, eclthrow(a;n), eclcatch(a;l)
Lemmas	decl-state wf, ma-valtype wf, bool wf, nat wf, ecl wf, eclcatch wf, eclthrow wf, eclact wf, eclrepeat wf, eclor wf, ecland wf, eclseq wf, Knd wf, eclbase wf, fpf wf, Id wf